Search Results

Documents authored by Sabel, David

Document
DOI: 10.4230/LIPIcs.FSCD.2018.28
Nominal Unification with Atom and Context Variables

Authors: Manfred Schmidt-Schauß and David Sabel

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
Automated deduction in higher-order program calculi, where properties of transformation rules are demanded, or confluence or other equational properties are requested, can often be done by syntactically computing overlaps (critical pairs) of reduction rules and transformation rules. Since higher-order calculi have alpha-equivalence as fundamental equivalence, the reasoning procedure must deal with it. We define ASD1-unification problems, which are higher-order equational unification problems employing variables for atoms, expressions and contexts, with additional distinct-variable constraints, and which have to be solved w.r.t. alpha-equivalence. Our proposal is to extend nominal unification to solve these unification problems. We succeeded in constructing the nominal unification algorithm NomUnifyASD. We show that NomUnifyASD is sound and complete for this problem class, and outputs a set of unifiers with constraints in nondeterministic polynomial time if the final constraints are satisfiable. We also show that solvability of the output constraints can be decided in NEXPTIME, and for a fixed number of context-variables in NP time. For terms without context-variables and atom-variables, NomUnifyASD runs in polynomial time, is unitary, and extends the classical problem by permitting distinct-variable constraints.
Cite as

Manfred Schmidt-Schauß and David Sabel. Nominal Unification with Atom and Context Variables. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 28:1-28:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{schmidtschau_et_al:LIPIcs.FSCD.2018.28,
  author =	{Schmidt-Schau{\ss}, Manfred and Sabel, David},
  title =	{{Nominal Unification with Atom and Context Variables}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{28:1--28:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.28},
  URN =		{urn:nbn:de:0030-drops-91983},
  doi =		{10.4230/LIPIcs.FSCD.2018.28},
  annote =	{Keywords: automated deduction, nominal unification, lambda calculus, functional programming}
}
Document
Complete Volume
DOI: 10.4230/OASIcs.WPTE.2015
OASIcs, Volume 46, WPTE'15, Complete Volume

Authors: Yuki Chiba, Santiago Escobar, Naoki Nishida, David Sabel, and Manfred Schmidt-Schauß

Published in: OASIcs, Volume 46, 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)

Abstract
OASIcs, Volume 46, WPTE'15, Complete Volume
Cite as

2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015). Open Access Series in Informatics (OASIcs), Volume 46, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Proceedings{chiba_et_al:OASIcs.WPTE.2015,
  title =	{{OASIcs, Volume 46, WPTE'15, Complete Volume}},
  booktitle =	{2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-94-1},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{46},
  editor =	{Chiba, Yuki and Escobar, Santiago and Nishida, Naoki and Sabel, David and Schmidt-Schau{\ss}, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2015},
  URN =		{urn:nbn:de:0030-drops-52644},
  doi =		{10.4230/OASIcs.WPTE.2015},
  annote =	{Keywords: Conference proceedings, Concurrent Programming, Formal Definitions and Theory, Specifying and Verifying and Reasoning about Programs, Semantics of Programming Languages, Mathematical Logic, Grammars and Other Rewriting Systems, Deduction and Theorem Proving}
}
Document
DOI: 10.4230/LIPIcs.RTA.2015.285
Transforming Cycle Rewriting into String Rewriting

Authors: David Sabel and Hans Zantema

Published in: LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)

Abstract
We present new techniques to prove termination of cycle rewriting, that is, string rewriting on cycles, which are strings in which the start and end are connected. Our main technique is to transform cycle rewriting into string rewriting and then apply state of the art techniques to prove termination of the string rewrite system. We present three such transformations, and prove for all of them that they are sound and complete. Apart from this transformational approach, we extend the use of matrix interpretations as was studied before. We present several experiments showing that often our new techniques succeed where earlier techniques fail.
Cite as

David Sabel and Hans Zantema. Transforming Cycle Rewriting into String Rewriting. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 285-300, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{sabel_et_al:LIPIcs.RTA.2015.285,
  author =	{Sabel, David and Zantema, Hans},
  title =	{{Transforming Cycle Rewriting into String Rewriting}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{285--300},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.285},
  URN =		{urn:nbn:de:0030-drops-52032},
  doi =		{10.4230/LIPIcs.RTA.2015.285},
  annote =	{Keywords: rewriting systems, string rewriting, termination}
}
Document
Front Matter
DOI: 10.4230/OASIcs.WPTE.2015.i
Frontmatter, Table of Contents, Preface, Workshop Organization

Authors: Yuki Chiba, Santiago Escobar, Naoki Nishida, David Sabel, and Manfred Schmidt-Schauß

Published in: OASIcs, Volume 46, 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)

Abstract
Frontmatter, Table of Contents, Preface, Workshop Organization
Cite as

2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015). Open Access Series in Informatics (OASIcs), Volume 46, pp. i-xvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{chiba_et_al:OASIcs.WPTE.2015.i,
  author =	{Chiba, Yuki and Escobar, Santiago and Nishida, Naoki and Sabel, David and Schmidt-Schau{\ss}, Manfred},
  title =	{{Frontmatter, Table of Contents, Preface, Workshop Organization}},
  booktitle =	{2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)},
  pages =	{i--xvi},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-94-1},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{46},
  editor =	{Chiba, Yuki and Escobar, Santiago and Nishida, Naoki and Sabel, David and Schmidt-Schau{\ss}, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2015.i},
  URN =		{urn:nbn:de:0030-drops-51765},
  doi =		{10.4230/OASIcs.WPTE.2015.i},
  annote =	{Keywords: Frontmatter, Table of Contents, Preface, Workshop Organization}
}
Document
DOI: 10.4230/OASIcs.WPTE.2015.31
Observing Success in the Pi-Calculus

Authors: David Sabel and Manfred Schmidt-Schauß

Published in: OASIcs, Volume 46, 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)

Abstract
A contextual semantics - defined in terms of successful termination and may- and should-convergence - is analyzed in the synchronous pi-calculus with replication and a constant Stop to denote success. The contextual ordering is analyzed, some nontrivial process equivalences are proved, and proof tools for showing contextual equivalences are provided. Among them are a context lemma and new notions of sound applicative similarities for may- and should-convergence. A further result is that contextual equivalence in the pi-calculus with Stop conservatively extends barbed testing equivalence in the (Stop-free) pi-calculus and thus results on contextual equivalence can be transferred to the (Stop-free) pi-calculus with barbed testing equivalence.
Cite as

David Sabel and Manfred Schmidt-Schauß. Observing Success in the Pi-Calculus. In 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015). Open Access Series in Informatics (OASIcs), Volume 46, pp. 31-46, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{sabel_et_al:OASIcs.WPTE.2015.31,
  author =	{Sabel, David and Schmidt-Schau{\ss}, Manfred},
  title =	{{Observing Success in the Pi-Calculus}},
  booktitle =	{2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)},
  pages =	{31--46},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-94-1},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{46},
  editor =	{Chiba, Yuki and Escobar, Santiago and Nishida, Naoki and Sabel, David and Schmidt-Schau{\ss}, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2015.31},
  URN =		{urn:nbn:de:0030-drops-51808},
  doi =		{10.4230/OASIcs.WPTE.2015.31},
  annote =	{Keywords: Concurrency, Process calculi, Pi-calculus, Rewriting, Semantics}
}
Document
Complete Volume
DOI: 10.4230/OASIcs.WPTE.2014
OASIcs, Volume 40, WPTE'14, Complete Volume

Authors: Manfred Schmidt-Schauß, Masahiko Sakai, David Sabel, and Yuki Chiba

Published in: OASIcs, Volume 40, First International Workshop on Rewriting Techniques for Program Transformations and Evaluation (2014)

Abstract
OASIcs, Volume 40, WPTE'14, Complete Volume
Cite as

First International Workshop on Rewriting Techniques for Program Transformations and Evaluation. Open Access Series in Informatics (OASIcs), Volume 40, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Proceedings{schmidtschau_et_al:OASIcs.WPTE.2014,
  title =	{{OASIcs, Volume 40, WPTE'14, Complete Volume}},
  booktitle =	{First International Workshop on Rewriting Techniques for Program Transformations and Evaluation},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-70-5},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{40},
  editor =	{Schmidt-Schau{\ss}, Manfred and Sakai, Masahiko and Sabel, David and Chiba, Yuki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2014},
  URN =		{urn:nbn:de:0030-drops-46216},
  doi =		{10.4230/OASIcs.WPTE.2014},
  annote =	{Keywords: Conference proceedings, Formal Definitions and Theory, Translator writing systems and compiler generators, Specifying and Verifying and Reasoning about Programs, Semantics of Programming Languages, Mathematical Logic, Grammars and Other Rewriting Systems}
}
Document
Front Matter
DOI: 10.4230/OASIcs.WPTE.2014.i
Frontmatter, Table of Contents, Preface, Workshop Organization

Authors: Manfred Schmidt-Schauß, Masahiko Sakai, David Sabel, and Yuki Chiba

Published in: OASIcs, Volume 40, First International Workshop on Rewriting Techniques for Program Transformations and Evaluation (2014)

Abstract
Frontmatter, Table of Contents, Preface, Workshop Organization
Cite as

First International Workshop on Rewriting Techniques for Program Transformations and Evaluation. Open Access Series in Informatics (OASIcs), Volume 40, pp. i-xv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{schmidtschau_et_al:OASIcs.WPTE.2014.i,
  author =	{Schmidt-Schau{\ss}, Manfred and Sakai, Masahiko and Sabel, David and Chiba, Yuki},
  title =	{{Frontmatter, Table of Contents, Preface, Workshop Organization}},
  booktitle =	{First International Workshop on Rewriting Techniques for Program Transformations and Evaluation},
  pages =	{i--xv},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-70-5},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{40},
  editor =	{Schmidt-Schau{\ss}, Manfred and Sakai, Masahiko and Sabel, David and Chiba, Yuki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2014.i},
  URN =		{urn:nbn:de:0030-drops-45814},
  doi =		{10.4230/OASIcs.WPTE.2014.i},
  annote =	{Keywords: Frontmatter, Table of Contents, Preface, Workshop Organization}
}
Document
DOI: 10.4230/OASIcs.WPTE.2014.51
Structural Rewriting in the pi-Calculus

Authors: David Sabel

Published in: OASIcs, Volume 40, First International Workshop on Rewriting Techniques for Program Transformations and Evaluation (2014)

Abstract
We consider reduction in the synchronous pi-calculus with replication, without sums. Usual definitions of reduction in the pi-calculus use a closure w.r.t. structural congruence of processes. In this paper we operationalize structural congruence by providing a reduction relation for pi-processes which also performs necessary structural conversions explicitly by rewrite rules. As we show, a subset of structural congruence axioms is sufficient. We show that our rewrite strategy is equivalent to the usual strategy including structural congruence w.r.t.the observation of barbs and thus w.r.t. may- and should-testing equivalence in the pi-calculus.
Cite as

David Sabel. Structural Rewriting in the pi-Calculus. In First International Workshop on Rewriting Techniques for Program Transformations and Evaluation. Open Access Series in Informatics (OASIcs), Volume 40, pp. 51-62, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{sabel:OASIcs.WPTE.2014.51,
  author =	{Sabel, David},
  title =	{{Structural Rewriting in the pi-Calculus}},
  booktitle =	{First International Workshop on Rewriting Techniques for Program Transformations and Evaluation},
  pages =	{51--62},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-70-5},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{40},
  editor =	{Schmidt-Schau{\ss}, Manfred and Sakai, Masahiko and Sabel, David and Chiba, Yuki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2014.51},
  URN =		{urn:nbn:de:0030-drops-45827},
  doi =		{10.4230/OASIcs.WPTE.2014.51},
  annote =	{Keywords: Process calculi, Rewriting, Semantics}
}
Document
Preliminary Report
DOI: 10.4230/OASIcs.WPTE.2014.63
Contextual Equivalences in Call-by-Need and Call-By-Name Polymorphically Typed Calculi (Preliminary Report)

Authors: Manfred Schmidt-Schauß and David Sabel

Published in: OASIcs, Volume 40, First International Workshop on Rewriting Techniques for Program Transformations and Evaluation (2014)

Abstract
This paper presents a call-by-need polymorphically typed lambda-calculus with letrec, case, constructors and seq. The typing of the calculus is modelled in a system-F style. Contextual equivalence is used as semantics of expressions. We also define a call-by-name variant without letrec. We adapt several tools and criteria for recognizing correct program transformations to polymorphic typing, in particular an inductive applicative simulation.
Cite as

Manfred Schmidt-Schauß and David Sabel. Contextual Equivalences in Call-by-Need and Call-By-Name Polymorphically Typed Calculi (Preliminary Report). In First International Workshop on Rewriting Techniques for Program Transformations and Evaluation. Open Access Series in Informatics (OASIcs), Volume 40, pp. 63-74, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{schmidtschau_et_al:OASIcs.WPTE.2014.63,
  author =	{Schmidt-Schau{\ss}, Manfred and Sabel, David},
  title =	{{Contextual Equivalences in Call-by-Need and Call-By-Name Polymorphically Typed Calculi}},
  booktitle =	{First International Workshop on Rewriting Techniques for Program Transformations and Evaluation},
  pages =	{63--74},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-70-5},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{40},
  editor =	{Schmidt-Schau{\ss}, Manfred and Sakai, Masahiko and Sabel, David and Chiba, Yuki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2014.63},
  URN =		{urn:nbn:de:0030-drops-45839},
  doi =		{10.4230/OASIcs.WPTE.2014.63},
  annote =	{Keywords: functional programming, polymorphic typing, contextual equivalence, semantics}
}
Document
DOI: 10.4230/LIPIcs.RTA.2013.239
Extending Abramsky's Lazy Lambda Calculus: (Non)-Conservativity of Embeddings

Authors: Manfred Schmidt-Schauß, Elena Machkasova, and David Sabel

Published in: LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013)

Abstract
Our motivation is the question whether the lazy lambda calculus, a pure lambda calculus with the leftmost outermost rewriting strategy, considered under observational semantics, or extensions thereof, are an adequate model for semantic equivalences in real-world purely functional programming languages, in particular for a pure core language of Haskell. We explore several extensions of the lazy lambda calculus: addition of a seq-operator, addition of data constructors and case-expressions, and their combination, focusing on conservativity of these extensions. In addition to untyped calculi, we study their monomorphically and polymorphically typed versions. For most of the extensions we obtain non-conservativity which we prove by providing counterexamples. However, we prove conservativity of the extension by data constructors and case in the monomorphically typed scenario.
Cite as

Manfred Schmidt-Schauß, Elena Machkasova, and David Sabel. Extending Abramsky's Lazy Lambda Calculus: (Non)-Conservativity of Embeddings. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 239-254, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{schmidtschau_et_al:LIPIcs.RTA.2013.239,
  author =	{Schmidt-Schau{\ss}, Manfred and Machkasova, Elena and Sabel, David},
  title =	{{Extending Abramsky's Lazy Lambda Calculus: (Non)-Conservativity of Embeddings}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{239--254},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.239},
  URN =		{urn:nbn:de:0030-drops-40651},
  doi =		{10.4230/LIPIcs.RTA.2013.239},
  annote =	{Keywords: lazy lambda calculus, contextual semantics, conservativity}
}
Document
DOI: 10.4230/LIPIcs.RTA.2013.255
Algorithms for Extended Alpha-Equivalence and Complexity

Authors: Manfred Schmidt-Schauß, Conrad Rau, and David Sabel

Published in: LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013)

Abstract
Equality of expressions in lambda-calculi, higher-order programming languages, higher-order programming calculi and process calculi is defined as alpha-equivalence. Permutability of bindings in let-constructs and structural congruence axioms extend alpha-equivalence. We analyse these extended alpha-equivalences and show that there are calculi with polynomial time algorithms, that a multiple-binding "let" may make alpha-equivalence as hard as finding graph-isomorphisms, and that the replication operator in the pi-calculus may lead to an EXPSPACE-hard alpha-equivalence problem.
Cite as

Manfred Schmidt-Schauß, Conrad Rau, and David Sabel. Algorithms for Extended Alpha-Equivalence and Complexity. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 255-270, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{schmidtschau_et_al:LIPIcs.RTA.2013.255,
  author =	{Schmidt-Schau{\ss}, Manfred and Rau, Conrad and Sabel, David},
  title =	{{Algorithms for Extended Alpha-Equivalence and Complexity}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{255--270},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.255},
  URN =		{urn:nbn:de:0030-drops-40667},
  doi =		{10.4230/LIPIcs.RTA.2013.255},
  annote =	{Keywords: alpha-equivalence, higher-order calculi, deduction, pi-calculus}
}
Document
DOI: 10.4230/LIPIcs.RTA.2010.295
Simulation in the Call-by-Need Lambda-Calculus with letrec

Authors: Manfred Schmidt-Schauss, David Sabel, and Elena Machkasova

Published in: LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010)

Abstract
This paper shows the equivalence of applicative similarity and contextual approximation, and hence also of bisimilarity and contextual equivalence, in the deterministic call-by-need lambda calculus with letrec. Bisimilarity simplifies equivalence proofs in the calculus and opens a way for more convenient correctness proofs for program transformations. Although this property may be a natural one to expect, to the best of our knowledge, this paper is the first one providing a proof. The proof technique is to transfer the contextual approximation into Abramsky's lazy lambda calculus by a fully abstract and surjective translation. This also shows that the natural embedding of Abramsky's lazy lambda calculus into the call-by-need lambda calculus with letrec is an isomorphism between the respective term-models. We show that the equivalence property proven in this paper transfers to a call-by-need letrec calculus developed by Ariola and Felleisen.
Cite as

Manfred Schmidt-Schauss, David Sabel, and Elena Machkasova. Simulation in the Call-by-Need Lambda-Calculus with letrec. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 295-310, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{schmidtschauss_et_al:LIPIcs.RTA.2010.295,
  author =	{Schmidt-Schauss, Manfred and Sabel, David and Machkasova, Elena},
  title =	{{Simulation in the Call-by-Need Lambda-Calculus with letrec}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{295--310},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Lynch, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.295},
  URN =		{urn:nbn:de:0030-drops-26593},
  doi =		{10.4230/LIPIcs.RTA.2010.295},
  annote =	{Keywords: Lambda calculus, semantics, contextual equivalence, bisimulation,call-by-need}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact